YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Weak Trs: { #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add following dependency tuples: Strict DPs: { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_7(append^#(@xs, @ys)) , append#1^#(nil(), @ys) -> c_8() , appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_10(appendD^#(@xs, @ys)) , appendD#1^#(nil(), @ys) -> c_11() , quicksort^#(@l) -> c_12(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_13(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#1^#(nil()) -> c_14() , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_16(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) , split#1^#(nil(), @pivot) -> c_23() , quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_18(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#1^#(nil()) -> c_19() , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_21(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) , splitD#1^#(nil(), @pivot) -> c_28() , split#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_24(split#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , split#3^#(#false(), @ls, @rs, @x) -> c_25() , split#3^#(#true(), @ls, @rs, @x) -> c_26() , splitD#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_29(splitD#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , splitD#3^#(#false(), @ls, @rs, @x) -> c_30() , splitD#3^#(#true(), @ls, @rs, @x) -> c_31() } Weak DPs: { #ckgt^#(#EQ()) -> c_44() , #ckgt^#(#GT()) -> c_45() , #ckgt^#(#LT()) -> c_46() , #compare^#(#0(), #0()) -> c_32() , #compare^#(#0(), #neg(@y)) -> c_33() , #compare^#(#0(), #pos(@y)) -> c_34() , #compare^#(#0(), #s(@y)) -> c_35() , #compare^#(#neg(@x), #0()) -> c_36() , #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_38() , #compare^#(#pos(@x), #0()) -> c_39() , #compare^#(#pos(@x), #neg(@y)) -> c_40() , #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_42() , #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() , #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_7(append^#(@xs, @ys)) , append#1^#(nil(), @ys) -> c_8() , appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_10(appendD^#(@xs, @ys)) , appendD#1^#(nil(), @ys) -> c_11() , quicksort^#(@l) -> c_12(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_13(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#1^#(nil()) -> c_14() , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_16(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) , split#1^#(nil(), @pivot) -> c_23() , quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_18(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#1^#(nil()) -> c_19() , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_21(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) , splitD#1^#(nil(), @pivot) -> c_28() , split#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_24(split#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , split#3^#(#false(), @ls, @rs, @x) -> c_25() , split#3^#(#true(), @ls, @rs, @x) -> c_26() , splitD#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_29(splitD#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , splitD#3^#(#false(), @ls, @rs, @x) -> c_30() , splitD#3^#(#true(), @ls, @rs, @x) -> c_31() } Weak DPs: { #ckgt^#(#EQ()) -> c_44() , #ckgt^#(#GT()) -> c_45() , #ckgt^#(#LT()) -> c_46() , #compare^#(#0(), #0()) -> c_32() , #compare^#(#0(), #neg(@y)) -> c_33() , #compare^#(#0(), #pos(@y)) -> c_34() , #compare^#(#0(), #s(@y)) -> c_35() , #compare^#(#neg(@x), #0()) -> c_36() , #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_38() , #compare^#(#pos(@x), #0()) -> c_39() , #compare^#(#pos(@x), #neg(@y)) -> c_40() , #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_42() , #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Consider the dependency graph 1: #abs^#(#0()) -> c_1() 2: #abs^#(#neg(@x)) -> c_2() 3: #abs^#(#pos(@x)) -> c_3() 4: #abs^#(#s(@x)) -> c_4() 5: #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) -->_2 #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) :46 -->_2 #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) :44 -->_2 #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) :40 -->_2 #compare^#(#s(@x), #0()) -> c_42() :45 -->_2 #compare^#(#pos(@x), #neg(@y)) -> c_40() :43 -->_2 #compare^#(#pos(@x), #0()) -> c_39() :42 -->_2 #compare^#(#neg(@x), #pos(@y)) -> c_38() :41 -->_2 #compare^#(#neg(@x), #0()) -> c_36() :39 -->_2 #compare^#(#0(), #s(@y)) -> c_35() :38 -->_2 #compare^#(#0(), #pos(@y)) -> c_34() :37 -->_2 #compare^#(#0(), #neg(@y)) -> c_33() :36 -->_2 #compare^#(#0(), #0()) -> c_32() :35 -->_1 #ckgt^#(#LT()) -> c_46() :34 -->_1 #ckgt^#(#GT()) -> c_45() :33 -->_1 #ckgt^#(#EQ()) -> c_44() :32 6: append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) -->_1 append#1^#(::(@x, @xs), @ys) -> c_7(append^#(@xs, @ys)) :7 -->_1 append#1^#(nil(), @ys) -> c_8() :8 7: append#1^#(::(@x, @xs), @ys) -> c_7(append^#(@xs, @ys)) -->_1 append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) :6 8: append#1^#(nil(), @ys) -> c_8() 9: appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) -->_1 appendD#1^#(::(@x, @xs), @ys) -> c_10(appendD^#(@xs, @ys)) :10 -->_1 appendD#1^#(nil(), @ys) -> c_11() :11 10: appendD#1^#(::(@x, @xs), @ys) -> c_10(appendD^#(@xs, @ys)) -->_1 appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) :9 11: appendD#1^#(nil(), @ys) -> c_11() 12: quicksort^#(@l) -> c_12(quicksort#1^#(@l)) -->_1 quicksort#1^#(::(@z, @zs)) -> c_13(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) :13 -->_1 quicksort#1^#(nil()) -> c_14() :14 13: quicksort#1^#(::(@z, @zs)) -> c_13(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) -->_2 split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) :16 -->_1 quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_16(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) :15 14: quicksort#1^#(nil()) -> c_14() 15: quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_16(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) -->_3 quicksort^#(@l) -> c_12(quicksort#1^#(@l)) :12 -->_2 quicksort^#(@l) -> c_12(quicksort#1^#(@l)) :12 -->_1 append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) :6 16: split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) -->_1 split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) :17 -->_1 split#1^#(nil(), @pivot) -> c_23() :18 17: split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) -->_1 split#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_24(split#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) :26 -->_2 split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) :16 18: split#1^#(nil(), @pivot) -> c_23() 19: quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) -->_1 quicksortD#1^#(::(@z, @zs)) -> c_18(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) :20 -->_1 quicksortD#1^#(nil()) -> c_19() :21 20: quicksortD#1^#(::(@z, @zs)) -> c_18(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) -->_2 splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) :23 -->_1 quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_21(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) :22 21: quicksortD#1^#(nil()) -> c_19() 22: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_21(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) -->_3 quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) :19 -->_2 quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) :19 -->_1 appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) :9 23: splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) -->_1 splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) :24 -->_1 splitD#1^#(nil(), @pivot) -> c_28() :25 24: splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) -->_1 splitD#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_29(splitD#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) :29 -->_2 splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) :23 25: splitD#1^#(nil(), @pivot) -> c_28() 26: split#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_24(split#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) -->_1 split#3^#(#true(), @ls, @rs, @x) -> c_26() :28 -->_1 split#3^#(#false(), @ls, @rs, @x) -> c_25() :27 -->_2 #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) :5 27: split#3^#(#false(), @ls, @rs, @x) -> c_25() 28: split#3^#(#true(), @ls, @rs, @x) -> c_26() 29: splitD#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_29(splitD#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) -->_1 splitD#3^#(#true(), @ls, @rs, @x) -> c_31() :31 -->_1 splitD#3^#(#false(), @ls, @rs, @x) -> c_30() :30 -->_2 #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) :5 30: splitD#3^#(#false(), @ls, @rs, @x) -> c_30() 31: splitD#3^#(#true(), @ls, @rs, @x) -> c_31() 32: #ckgt^#(#EQ()) -> c_44() 33: #ckgt^#(#GT()) -> c_45() 34: #ckgt^#(#LT()) -> c_46() 35: #compare^#(#0(), #0()) -> c_32() 36: #compare^#(#0(), #neg(@y)) -> c_33() 37: #compare^#(#0(), #pos(@y)) -> c_34() 38: #compare^#(#0(), #s(@y)) -> c_35() 39: #compare^#(#neg(@x), #0()) -> c_36() 40: #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) -->_1 #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) :46 -->_1 #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) :44 -->_1 #compare^#(#s(@x), #0()) -> c_42() :45 -->_1 #compare^#(#pos(@x), #neg(@y)) -> c_40() :43 -->_1 #compare^#(#pos(@x), #0()) -> c_39() :42 -->_1 #compare^#(#neg(@x), #pos(@y)) -> c_38() :41 -->_1 #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) :40 -->_1 #compare^#(#neg(@x), #0()) -> c_36() :39 -->_1 #compare^#(#0(), #s(@y)) -> c_35() :38 -->_1 #compare^#(#0(), #pos(@y)) -> c_34() :37 -->_1 #compare^#(#0(), #neg(@y)) -> c_33() :36 -->_1 #compare^#(#0(), #0()) -> c_32() :35 41: #compare^#(#neg(@x), #pos(@y)) -> c_38() 42: #compare^#(#pos(@x), #0()) -> c_39() 43: #compare^#(#pos(@x), #neg(@y)) -> c_40() 44: #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) -->_1 #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) :46 -->_1 #compare^#(#s(@x), #0()) -> c_42() :45 -->_1 #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) :44 -->_1 #compare^#(#pos(@x), #neg(@y)) -> c_40() :43 -->_1 #compare^#(#pos(@x), #0()) -> c_39() :42 -->_1 #compare^#(#neg(@x), #pos(@y)) -> c_38() :41 -->_1 #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) :40 -->_1 #compare^#(#neg(@x), #0()) -> c_36() :39 -->_1 #compare^#(#0(), #s(@y)) -> c_35() :38 -->_1 #compare^#(#0(), #pos(@y)) -> c_34() :37 -->_1 #compare^#(#0(), #neg(@y)) -> c_33() :36 -->_1 #compare^#(#0(), #0()) -> c_32() :35 45: #compare^#(#s(@x), #0()) -> c_42() 46: #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) -->_1 #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) :46 -->_1 #compare^#(#s(@x), #0()) -> c_42() :45 -->_1 #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) :44 -->_1 #compare^#(#pos(@x), #neg(@y)) -> c_40() :43 -->_1 #compare^#(#pos(@x), #0()) -> c_39() :42 -->_1 #compare^#(#neg(@x), #pos(@y)) -> c_38() :41 -->_1 #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) :40 -->_1 #compare^#(#neg(@x), #0()) -> c_36() :39 -->_1 #compare^#(#0(), #s(@y)) -> c_35() :38 -->_1 #compare^#(#0(), #pos(@y)) -> c_34() :37 -->_1 #compare^#(#0(), #neg(@y)) -> c_33() :36 -->_1 #compare^#(#0(), #0()) -> c_32() :35 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { #abs^#(#0()) -> c_1() , #abs^#(#neg(@x)) -> c_2() , #abs^#(#pos(@x)) -> c_3() , #abs^#(#s(@x)) -> c_4() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_7(append^#(@xs, @ys)) , append#1^#(nil(), @ys) -> c_8() , appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_10(appendD^#(@xs, @ys)) , appendD#1^#(nil(), @ys) -> c_11() , quicksort^#(@l) -> c_12(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_13(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#1^#(nil()) -> c_14() , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_16(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) , split#1^#(nil(), @pivot) -> c_23() , quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_18(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#1^#(nil()) -> c_19() , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_21(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) , splitD#1^#(nil(), @pivot) -> c_28() , split#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_24(split#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , split#3^#(#false(), @ls, @rs, @x) -> c_25() , split#3^#(#true(), @ls, @rs, @x) -> c_26() , splitD#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_29(splitD#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , splitD#3^#(#false(), @ls, @rs, @x) -> c_30() , splitD#3^#(#true(), @ls, @rs, @x) -> c_31() } Weak DPs: { #ckgt^#(#EQ()) -> c_44() , #ckgt^#(#GT()) -> c_45() , #ckgt^#(#LT()) -> c_46() , #compare^#(#0(), #0()) -> c_32() , #compare^#(#0(), #neg(@y)) -> c_33() , #compare^#(#0(), #pos(@y)) -> c_34() , #compare^#(#0(), #s(@y)) -> c_35() , #compare^#(#neg(@x), #0()) -> c_36() , #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_38() , #compare^#(#pos(@x), #0()) -> c_39() , #compare^#(#pos(@x), #neg(@y)) -> c_40() , #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_42() , #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {1,4,7,10,14,17,21,23,24,26,27} by applications of Pre({1,4,7,10,14,17,21,23,24,26,27}) = {2,5,8,12,15,19,22,25}. Here rules are labeled as follows: DPs: { 1: #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 2: append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) , 3: append#1^#(::(@x, @xs), @ys) -> c_7(append^#(@xs, @ys)) , 4: append#1^#(nil(), @ys) -> c_8() , 5: appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) , 6: appendD#1^#(::(@x, @xs), @ys) -> c_10(appendD^#(@xs, @ys)) , 7: appendD#1^#(nil(), @ys) -> c_11() , 8: quicksort^#(@l) -> c_12(quicksort#1^#(@l)) , 9: quicksort#1^#(::(@z, @zs)) -> c_13(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , 10: quicksort#1^#(nil()) -> c_14() , 11: quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_16(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , 12: split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) , 13: split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) , 14: split#1^#(nil(), @pivot) -> c_23() , 15: quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) , 16: quicksortD#1^#(::(@z, @zs)) -> c_18(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , 17: quicksortD#1^#(nil()) -> c_19() , 18: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_21(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , 19: splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) , 20: splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) , 21: splitD#1^#(nil(), @pivot) -> c_28() , 22: split#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_24(split#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , 23: split#3^#(#false(), @ls, @rs, @x) -> c_25() , 24: split#3^#(#true(), @ls, @rs, @x) -> c_26() , 25: splitD#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_29(splitD#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , 26: splitD#3^#(#false(), @ls, @rs, @x) -> c_30() , 27: splitD#3^#(#true(), @ls, @rs, @x) -> c_31() , 28: #ckgt^#(#EQ()) -> c_44() , 29: #ckgt^#(#GT()) -> c_45() , 30: #ckgt^#(#LT()) -> c_46() , 31: #compare^#(#0(), #0()) -> c_32() , 32: #compare^#(#0(), #neg(@y)) -> c_33() , 33: #compare^#(#0(), #pos(@y)) -> c_34() , 34: #compare^#(#0(), #s(@y)) -> c_35() , 35: #compare^#(#neg(@x), #0()) -> c_36() , 36: #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) , 37: #compare^#(#neg(@x), #pos(@y)) -> c_38() , 38: #compare^#(#pos(@x), #0()) -> c_39() , 39: #compare^#(#pos(@x), #neg(@y)) -> c_40() , 40: #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) , 41: #compare^#(#s(@x), #0()) -> c_42() , 42: #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_7(append^#(@xs, @ys)) , appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_10(appendD^#(@xs, @ys)) , quicksort^#(@l) -> c_12(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_13(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_16(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) , quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_18(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_21(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) , split#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_24(split#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , splitD#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_29(splitD#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) } Weak DPs: { #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_44() , #ckgt^#(#GT()) -> c_45() , #ckgt^#(#LT()) -> c_46() , #compare^#(#0(), #0()) -> c_32() , #compare^#(#0(), #neg(@y)) -> c_33() , #compare^#(#0(), #pos(@y)) -> c_34() , #compare^#(#0(), #s(@y)) -> c_35() , #compare^#(#neg(@x), #0()) -> c_36() , #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_38() , #compare^#(#pos(@x), #0()) -> c_39() , #compare^#(#pos(@x), #neg(@y)) -> c_40() , #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_42() , #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) , append#1^#(nil(), @ys) -> c_8() , appendD#1^#(nil(), @ys) -> c_11() , quicksort#1^#(nil()) -> c_14() , split#1^#(nil(), @pivot) -> c_23() , quicksortD#1^#(nil()) -> c_19() , splitD#1^#(nil(), @pivot) -> c_28() , split#3^#(#false(), @ls, @rs, @x) -> c_25() , split#3^#(#true(), @ls, @rs, @x) -> c_26() , splitD#3^#(#false(), @ls, @rs, @x) -> c_30() , splitD#3^#(#true(), @ls, @rs, @x) -> c_31() } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {15,16} by applications of Pre({15,16}) = {9,14}. Here rules are labeled as follows: DPs: { 1: append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) , 2: append#1^#(::(@x, @xs), @ys) -> c_7(append^#(@xs, @ys)) , 3: appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) , 4: appendD#1^#(::(@x, @xs), @ys) -> c_10(appendD^#(@xs, @ys)) , 5: quicksort^#(@l) -> c_12(quicksort#1^#(@l)) , 6: quicksort#1^#(::(@z, @zs)) -> c_13(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , 7: quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_16(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , 8: split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) , 9: split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) , 10: quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) , 11: quicksortD#1^#(::(@z, @zs)) -> c_18(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , 12: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_21(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , 13: splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) , 14: splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) , 15: split#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_24(split#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , 16: splitD#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_29(splitD#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , 17: #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , 18: #ckgt^#(#EQ()) -> c_44() , 19: #ckgt^#(#GT()) -> c_45() , 20: #ckgt^#(#LT()) -> c_46() , 21: #compare^#(#0(), #0()) -> c_32() , 22: #compare^#(#0(), #neg(@y)) -> c_33() , 23: #compare^#(#0(), #pos(@y)) -> c_34() , 24: #compare^#(#0(), #s(@y)) -> c_35() , 25: #compare^#(#neg(@x), #0()) -> c_36() , 26: #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) , 27: #compare^#(#neg(@x), #pos(@y)) -> c_38() , 28: #compare^#(#pos(@x), #0()) -> c_39() , 29: #compare^#(#pos(@x), #neg(@y)) -> c_40() , 30: #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) , 31: #compare^#(#s(@x), #0()) -> c_42() , 32: #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) , 33: append#1^#(nil(), @ys) -> c_8() , 34: appendD#1^#(nil(), @ys) -> c_11() , 35: quicksort#1^#(nil()) -> c_14() , 36: split#1^#(nil(), @pivot) -> c_23() , 37: quicksortD#1^#(nil()) -> c_19() , 38: splitD#1^#(nil(), @pivot) -> c_28() , 39: split#3^#(#false(), @ls, @rs, @x) -> c_25() , 40: split#3^#(#true(), @ls, @rs, @x) -> c_26() , 41: splitD#3^#(#false(), @ls, @rs, @x) -> c_30() , 42: splitD#3^#(#true(), @ls, @rs, @x) -> c_31() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_7(append^#(@xs, @ys)) , appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_10(appendD^#(@xs, @ys)) , quicksort^#(@l) -> c_12(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_13(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_16(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) , quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_18(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_21(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) } Weak DPs: { #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_44() , #ckgt^#(#GT()) -> c_45() , #ckgt^#(#LT()) -> c_46() , #compare^#(#0(), #0()) -> c_32() , #compare^#(#0(), #neg(@y)) -> c_33() , #compare^#(#0(), #pos(@y)) -> c_34() , #compare^#(#0(), #s(@y)) -> c_35() , #compare^#(#neg(@x), #0()) -> c_36() , #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_38() , #compare^#(#pos(@x), #0()) -> c_39() , #compare^#(#pos(@x), #neg(@y)) -> c_40() , #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_42() , #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) , append#1^#(nil(), @ys) -> c_8() , appendD#1^#(nil(), @ys) -> c_11() , quicksort#1^#(nil()) -> c_14() , split#1^#(nil(), @pivot) -> c_23() , quicksortD#1^#(nil()) -> c_19() , splitD#1^#(nil(), @pivot) -> c_28() , split#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_24(split#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , split#3^#(#false(), @ls, @rs, @x) -> c_25() , split#3^#(#true(), @ls, @rs, @x) -> c_26() , splitD#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_29(splitD#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , splitD#3^#(#false(), @ls, @rs, @x) -> c_30() , splitD#3^#(#true(), @ls, @rs, @x) -> c_31() } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { #greater^#(@x, @y) -> c_5(#ckgt^#(#compare(@x, @y)), #compare^#(@x, @y)) , #ckgt^#(#EQ()) -> c_44() , #ckgt^#(#GT()) -> c_45() , #ckgt^#(#LT()) -> c_46() , #compare^#(#0(), #0()) -> c_32() , #compare^#(#0(), #neg(@y)) -> c_33() , #compare^#(#0(), #pos(@y)) -> c_34() , #compare^#(#0(), #s(@y)) -> c_35() , #compare^#(#neg(@x), #0()) -> c_36() , #compare^#(#neg(@x), #neg(@y)) -> c_37(#compare^#(@y, @x)) , #compare^#(#neg(@x), #pos(@y)) -> c_38() , #compare^#(#pos(@x), #0()) -> c_39() , #compare^#(#pos(@x), #neg(@y)) -> c_40() , #compare^#(#pos(@x), #pos(@y)) -> c_41(#compare^#(@x, @y)) , #compare^#(#s(@x), #0()) -> c_42() , #compare^#(#s(@x), #s(@y)) -> c_43(#compare^#(@x, @y)) , append#1^#(nil(), @ys) -> c_8() , appendD#1^#(nil(), @ys) -> c_11() , quicksort#1^#(nil()) -> c_14() , split#1^#(nil(), @pivot) -> c_23() , quicksortD#1^#(nil()) -> c_19() , splitD#1^#(nil(), @pivot) -> c_28() , split#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_24(split#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , split#3^#(#false(), @ls, @rs, @x) -> c_25() , split#3^#(#true(), @ls, @rs, @x) -> c_26() , splitD#2^#(tuple#2(@ls, @rs), @pivot, @x) -> c_29(splitD#3^#(#greater(@x, @pivot), @ls, @rs, @x), #greater^#(@x, @pivot)) , splitD#3^#(#false(), @ls, @rs, @x) -> c_30() , splitD#3^#(#true(), @ls, @rs, @x) -> c_31() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { append^#(@l, @ys) -> c_6(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_7(append^#(@xs, @ys)) , appendD^#(@l, @ys) -> c_9(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_10(appendD^#(@xs, @ys)) , quicksort^#(@l) -> c_12(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_13(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_16(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_15(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) , quicksortD^#(@l) -> c_17(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_18(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_21(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_20(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { split#1^#(::(@x, @xs), @pivot) -> c_22(split#2^#(split(@pivot, @xs), @pivot, @x), split^#(@pivot, @xs)) , splitD#1^#(::(@x, @xs), @pivot) -> c_27(splitD#2^#(splitD(@pivot, @xs), @pivot, @x), splitD^#(@pivot, @xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) , quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component: Problem (R): ------------ Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Weak DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost Problem (S): ------------ Strict DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost Overall, the transformation results in the following sub-problem(s): Generated new problems: ----------------------- R) Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Weak DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost This problem was proven YES(O(1),O(n^2)). S) Strict DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost This problem was proven YES(O(1),O(n^2)). Proofs for generated problems: ------------------------------ R) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Weak DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We decompose the input problem according to the dependency graph into the upper component { quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) } and lower component { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Further, following extension rules are added to the lower component. { quicksort^#(@l) -> quicksort#1^#(@l) , quicksort#1^#(::(@z, @zs)) -> quicksort#2^#(split(@z, @zs), @z) , quicksort#1^#(::(@z, @zs)) -> split^#(@z, @zs) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> append^#(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@xs) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@ys) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { quicksort^#(@l) -> c_1(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_2(quicksort#2^#(split(@z, @zs), @z)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksort^#(@xs), quicksort^#(@ys)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We replace rewrite rules by usable rules: Weak Usable Rules: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , split(@pivot, @l) -> split#1(@l, @pivot) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { quicksort^#(@l) -> c_1(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_2(quicksort#2^#(split(@z, @zs), @z)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksort^#(@xs), quicksort^#(@ys)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , split(@pivot, @l) -> split#1(@l, @pivot) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 3: quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksort^#(@xs), quicksort^#(@ys)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#0] = [0] [#neg](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#s](x1) = [1] x1 + [1] [#greater](x1, x2) = [1] [#compare](x1, x2) = [1] [#ckgt](x1) = [1] x1 + [0] [append](x1, x2) = [0] [append#1](x1, x2) = [0] [::](x1, x2) = [1] x2 + [1] [nil] = [0] [quicksort](x1) = [0] [quicksort#1](x1) = [0] [split](x1, x2) = [1] x2 + [1] [quicksort#2](x1, x2) = [0] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [1] [split#1](x1, x2) = [1] x1 + [1] [split#2](x1, x2, x3) = [1] x1 + [1] [split#3](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1] x3 + [1] [#false] = [1] [#true] = [1] [#EQ] = [1] [#GT] = [1] [#LT] = [1] [#abs^#](x1) = [0] [#greater^#](x1, x2) = [0] [#ckgt^#](x1) = [0] [#compare^#](x1, x2) = [0] [append^#](x1, x2) = [0] [append#1^#](x1, x2) = [0] [appendD^#](x1, x2) = [0] [appendD#1^#](x1, x2) = [0] [quicksort^#](x1) = [1] x1 + [0] [quicksort#1^#](x1) = [1] x1 + [0] [quicksort#2^#](x1, x2) = [1] x1 + [0] [split^#](x1, x2) = [0] [split#1^#](x1, x2) = [0] [quicksortD^#](x1) = [0] [quicksortD#1^#](x1) = [0] [quicksortD#2^#](x1, x2) = [0] [splitD^#](x1, x2) = [0] [splitD#1^#](x1, x2) = [0] [split#2^#](x1, x2, x3) = [0] [split#3^#](x1, x2, x3, x4) = [0] [splitD#2^#](x1, x2, x3) = [0] [splitD#3^#](x1, x2, x3, x4) = [0] [c_5](x1) = [0] [c_6](x1, x2) = [0] [c_7](x1, x2, x3) = [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [c_3](x1, x2) = [1] x1 + [1] x2 + [0] This order satisfies following ordering constraints [#greater(@x, @y)] = [1] >= [1] = [#ckgt(#compare(@x, @y))] [#compare(#0(), #0())] = [1] >= [1] = [#EQ()] [#compare(#0(), #neg(@y))] = [1] >= [1] = [#GT()] [#compare(#0(), #pos(@y))] = [1] >= [1] = [#LT()] [#compare(#0(), #s(@y))] = [1] >= [1] = [#LT()] [#compare(#neg(@x), #0())] = [1] >= [1] = [#LT()] [#compare(#neg(@x), #neg(@y))] = [1] >= [1] = [#compare(@y, @x)] [#compare(#neg(@x), #pos(@y))] = [1] >= [1] = [#LT()] [#compare(#pos(@x), #0())] = [1] >= [1] = [#GT()] [#compare(#pos(@x), #neg(@y))] = [1] >= [1] = [#GT()] [#compare(#pos(@x), #pos(@y))] = [1] >= [1] = [#compare(@x, @y)] [#compare(#s(@x), #0())] = [1] >= [1] = [#GT()] [#compare(#s(@x), #s(@y))] = [1] >= [1] = [#compare(@x, @y)] [#ckgt(#EQ())] = [1] >= [1] = [#false()] [#ckgt(#GT())] = [1] >= [1] = [#true()] [#ckgt(#LT())] = [1] >= [1] = [#false()] [split(@pivot, @l)] = [1] @l + [1] >= [1] @l + [1] = [split#1(@l, @pivot)] [split#1(::(@x, @xs), @pivot)] = [1] @xs + [2] >= [1] @xs + [2] = [split#2(split(@pivot, @xs), @pivot, @x)] [split#1(nil(), @pivot)] = [1] >= [1] = [tuple#2(nil(), nil())] [split#2(tuple#2(@ls, @rs), @pivot, @x)] = [1] @ls + [1] @rs + [2] >= [1] @ls + [1] @rs + [2] = [split#3(#greater(@x, @pivot), @ls, @rs, @x)] [split#3(#false(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [2] >= [1] @ls + [1] @rs + [2] = [tuple#2(::(@x, @ls), @rs)] [split#3(#true(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [2] >= [1] @ls + [1] @rs + [2] = [tuple#2(@ls, ::(@x, @rs))] [quicksort^#(@l)] = [1] @l + [0] >= [1] @l + [0] = [c_1(quicksort#1^#(@l))] [quicksort#1^#(::(@z, @zs))] = [1] @zs + [1] >= [1] @zs + [1] = [c_2(quicksort#2^#(split(@z, @zs), @z))] [quicksort#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] > [1] @xs + [1] @ys + [0] = [c_3(quicksort^#(@xs), quicksort^#(@ys))] Consider the set of all dependency pairs DPs: { 1: quicksort^#(@l) -> c_1(quicksort#1^#(@l)) , 2: quicksort#1^#(::(@z, @zs)) -> c_2(quicksort#2^#(split(@z, @zs), @z)) , 3: quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksort^#(@xs), quicksort^#(@ys)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {3}. These cover all (indirect) predecessors of dependency pairs {1,2,3}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { quicksort^#(@l) -> c_1(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_2(quicksort#2^#(split(@z, @zs), @z)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksort^#(@xs), quicksort^#(@ys)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , split(@pivot, @l) -> split#1(@l, @pivot) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { quicksort^#(@l) -> c_1(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_2(quicksort#2^#(split(@z, @zs), @z)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksort^#(@xs), quicksort^#(@ys)) } We apply the transformation 'usablerules' on the sub-problem: Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , split(@pivot, @l) -> split#1(@l, @pivot) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Weak DPs: { quicksort^#(@l) -> quicksort#1^#(@l) , quicksort#1^#(::(@z, @zs)) -> quicksort#2^#(split(@z, @zs), @z) , quicksort#1^#(::(@z, @zs)) -> split^#(@z, @zs) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> append^#(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@xs) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@ys) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 4: split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) , 6: quicksort#1^#(::(@z, @zs)) -> quicksort#2^#(split(@z, @zs), @z) , 7: quicksort#1^#(::(@z, @zs)) -> split^#(@z, @zs) , 8: quicksort#2^#(tuple#2(@xs, @ys), @z) -> append^#(quicksort(@xs), ::(@z, quicksort(@ys))) } Trs: { quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_8) = {1}, Uargs(c_9) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#0] = [0] [#neg](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#s](x1) = [1] x1 + [1] [#greater](x1, x2) = [0] [#compare](x1, x2) = [0] [#ckgt](x1) = [1] x1 + [0] [append](x1, x2) = [1] x2 + [0] [append#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x2 + [1] [nil] = [0] [quicksort](x1) = [0] [quicksort#1](x1) = [1] [split](x1, x2) = [1] x2 + [0] [quicksort#2](x1, x2) = [0] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [split#1](x1, x2) = [1] x1 + [0] [split#2](x1, x2, x3) = [1] x1 + [1] [split#3](x1, x2, x3, x4) = [1] x2 + [1] x3 + [1] [#false] = [1] [#true] = [1] [#EQ] = [0] [#GT] = [0] [#LT] = [0] [#abs^#](x1) = [0] [#greater^#](x1, x2) = [0] [#ckgt^#](x1) = [0] [#compare^#](x1, x2) = [0] [append^#](x1, x2) = [0] [append#1^#](x1, x2) = [0] [appendD^#](x1, x2) = [0] [appendD#1^#](x1, x2) = [0] [quicksort^#](x1) = [1] x1 + [1] [quicksort#1^#](x1) = [1] x1 + [1] [quicksort#2^#](x1, x2) = [1] x1 + [1] [split^#](x1, x2) = [1] x2 + [0] [split#1^#](x1, x2) = [1] x1 + [0] [quicksortD^#](x1) = [0] [quicksortD#1^#](x1) = [0] [quicksortD#2^#](x1, x2) = [0] [splitD^#](x1, x2) = [0] [splitD#1^#](x1, x2) = [0] [split#2^#](x1, x2, x3) = [0] [split#3^#](x1, x2, x3, x4) = [0] [splitD#2^#](x1, x2, x3) = [0] [splitD#3^#](x1, x2, x3, x4) = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [c_8](x1) = [1] x1 + [0] [c_9](x1) = [1] x1 + [0] This order satisfies following ordering constraints [split(@pivot, @l)] = [1] @l + [0] >= [1] @l + [0] = [split#1(@l, @pivot)] [split#1(::(@x, @xs), @pivot)] = [1] @xs + [1] >= [1] @xs + [1] = [split#2(split(@pivot, @xs), @pivot, @x)] [split#1(nil(), @pivot)] = [0] >= [0] = [tuple#2(nil(), nil())] [split#2(tuple#2(@ls, @rs), @pivot, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [split#3(#greater(@x, @pivot), @ls, @rs, @x)] [split#3(#false(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [tuple#2(::(@x, @ls), @rs)] [split#3(#true(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [tuple#2(@ls, ::(@x, @rs))] [append^#(@l, @ys)] = [0] >= [0] = [c_1(append#1^#(@l, @ys))] [append#1^#(::(@x, @xs), @ys)] = [0] >= [0] = [c_2(append^#(@xs, @ys))] [quicksort^#(@l)] = [1] @l + [1] >= [1] @l + [1] = [quicksort#1^#(@l)] [quicksort#1^#(::(@z, @zs))] = [1] @zs + [2] > [1] @zs + [1] = [quicksort#2^#(split(@z, @zs), @z)] [quicksort#1^#(::(@z, @zs))] = [1] @zs + [2] > [1] @zs + [0] = [split^#(@z, @zs)] [quicksort#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] > [0] = [append^#(quicksort(@xs), ::(@z, quicksort(@ys)))] [quicksort#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] >= [1] @xs + [1] = [quicksort^#(@xs)] [quicksort#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] >= [1] @ys + [1] = [quicksort^#(@ys)] [split^#(@pivot, @l)] = [1] @l + [0] >= [1] @l + [0] = [c_8(split#1^#(@l, @pivot))] [split#1^#(::(@x, @xs), @pivot)] = [1] @xs + [1] > [1] @xs + [0] = [c_9(split^#(@pivot, @xs))] Consider the set of all dependency pairs DPs: { 1: append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , 2: append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , 3: split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , 4: split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) , 5: quicksort^#(@l) -> quicksort#1^#(@l) , 6: quicksort#1^#(::(@z, @zs)) -> quicksort#2^#(split(@z, @zs), @z) , 7: quicksort#1^#(::(@z, @zs)) -> split^#(@z, @zs) , 8: quicksort#2^#(tuple#2(@xs, @ys), @z) -> append^#(quicksort(@xs), ::(@z, quicksort(@ys))) , 9: quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@xs) , 10: quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@ys) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {4,6,7,8}. These cover all (indirect) predecessors of dependency pairs {3,4,5,6,7,8,9,10}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) } Weak DPs: { quicksort^#(@l) -> quicksort#1^#(@l) , quicksort#1^#(::(@z, @zs)) -> quicksort#2^#(split(@z, @zs), @z) , quicksort#1^#(::(@z, @zs)) -> split^#(@z, @zs) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> append^#(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@xs) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@ys) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { quicksort#1^#(::(@z, @zs)) -> split^#(@z, @zs) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) } Weak DPs: { quicksort^#(@l) -> quicksort#1^#(@l) , quicksort#1^#(::(@z, @zs)) -> quicksort#2^#(split(@z, @zs), @z) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> append^#(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@xs) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@ys) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , 5: quicksort#2^#(tuple#2(@xs, @ys), @z) -> append^#(quicksort(@xs), ::(@z, quicksort(@ys))) , 6: quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@xs) , 7: quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@ys) } Trs: { #compare(#0(), #0()) -> #EQ() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #pos(@y)) -> #LT() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#0] = [1] [#neg](x1) = [1] x1 + [1] [#pos](x1) = [1] x1 + [1] [#s](x1) = [1] x1 + [1] [#greater](x1, x2) = [1] [#compare](x1, x2) = [1] [#ckgt](x1) = [1] [append](x1, x2) = [1] x1 + [1] x2 + [0] [append#1](x1, x2) = [1] x1 + [1] x2 + [0] [::](x1, x2) = [1] x2 + [1] [nil] = [0] [quicksort](x1) = [1] x1 + [0] [quicksort#1](x1) = [1] x1 + [0] [split](x1, x2) = [1] x2 + [0] [quicksort#2](x1, x2) = [1] x1 + [1] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [split#1](x1, x2) = [1] x1 + [0] [split#2](x1, x2, x3) = [1] x1 + [1] [split#3](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1] x3 + [0] [#false] = [1] [#true] = [1] [#EQ] = [0] [#GT] = [1] [#LT] = [0] [#abs^#](x1) = [0] [#greater^#](x1, x2) = [0] [#ckgt^#](x1) = [0] [#compare^#](x1, x2) = [0] [append^#](x1, x2) = [1] x1 + [0] [append#1^#](x1, x2) = [1] x1 + [0] [appendD^#](x1, x2) = [0] [appendD#1^#](x1, x2) = [0] [quicksort^#](x1) = [1] x1 + [0] [quicksort#1^#](x1) = [1] x1 + [0] [quicksort#2^#](x1, x2) = [1] x1 + [1] [split^#](x1, x2) = [0] [split#1^#](x1, x2) = [0] [quicksortD^#](x1) = [0] [quicksortD#1^#](x1) = [0] [quicksortD#2^#](x1, x2) = [0] [splitD^#](x1, x2) = [0] [splitD#1^#](x1, x2) = [0] [split#2^#](x1, x2, x3) = [0] [split#3^#](x1, x2, x3, x4) = [0] [splitD#2^#](x1, x2, x3) = [0] [splitD#3^#](x1, x2, x3, x4) = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [c_8](x1) = [0] [c_9](x1) = [0] This order satisfies following ordering constraints [#greater(@x, @y)] = [1] >= [1] = [#ckgt(#compare(@x, @y))] [#ckgt(#EQ())] = [1] >= [1] = [#false()] [#ckgt(#GT())] = [1] >= [1] = [#true()] [#ckgt(#LT())] = [1] >= [1] = [#false()] [append(@l, @ys)] = [1] @l + [1] @ys + [0] >= [1] @l + [1] @ys + [0] = [append#1(@l, @ys)] [append#1(::(@x, @xs), @ys)] = [1] @xs + [1] @ys + [1] >= [1] @xs + [1] @ys + [1] = [::(@x, append(@xs, @ys))] [append#1(nil(), @ys)] = [1] @ys + [0] >= [1] @ys + [0] = [@ys] [quicksort(@l)] = [1] @l + [0] >= [1] @l + [0] = [quicksort#1(@l)] [quicksort#1(::(@z, @zs))] = [1] @zs + [1] >= [1] @zs + [1] = [quicksort#2(split(@z, @zs), @z)] [quicksort#1(nil())] = [0] >= [0] = [nil()] [split(@pivot, @l)] = [1] @l + [0] >= [1] @l + [0] = [split#1(@l, @pivot)] [quicksort#2(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] >= [1] @xs + [1] @ys + [1] = [append(quicksort(@xs), ::(@z, quicksort(@ys)))] [split#1(::(@x, @xs), @pivot)] = [1] @xs + [1] >= [1] @xs + [1] = [split#2(split(@pivot, @xs), @pivot, @x)] [split#1(nil(), @pivot)] = [0] >= [0] = [tuple#2(nil(), nil())] [split#2(tuple#2(@ls, @rs), @pivot, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [split#3(#greater(@x, @pivot), @ls, @rs, @x)] [split#3(#false(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [tuple#2(::(@x, @ls), @rs)] [split#3(#true(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [tuple#2(@ls, ::(@x, @rs))] [append^#(@l, @ys)] = [1] @l + [0] >= [1] @l + [0] = [c_1(append#1^#(@l, @ys))] [append#1^#(::(@x, @xs), @ys)] = [1] @xs + [1] > [1] @xs + [0] = [c_2(append^#(@xs, @ys))] [quicksort^#(@l)] = [1] @l + [0] >= [1] @l + [0] = [quicksort#1^#(@l)] [quicksort#1^#(::(@z, @zs))] = [1] @zs + [1] >= [1] @zs + [1] = [quicksort#2^#(split(@z, @zs), @z)] [quicksort#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] > [1] @xs + [0] = [append^#(quicksort(@xs), ::(@z, quicksort(@ys)))] [quicksort#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] > [1] @xs + [0] = [quicksort^#(@xs)] [quicksort#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] > [1] @ys + [0] = [quicksort^#(@ys)] Consider the set of all dependency pairs DPs: { 1: append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , 2: append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , 3: quicksort^#(@l) -> quicksort#1^#(@l) , 4: quicksort#1^#(::(@z, @zs)) -> quicksort#2^#(split(@z, @zs), @z) , 5: quicksort#2^#(tuple#2(@xs, @ys), @z) -> append^#(quicksort(@xs), ::(@z, quicksort(@ys))) , 6: quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@xs) , 7: quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@ys) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {2,5,6,7}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6,7}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> quicksort#1^#(@l) , quicksort#1^#(::(@z, @zs)) -> quicksort#2^#(split(@z, @zs), @z) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> append^#(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@xs) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@ys) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> quicksort#1^#(@l) , quicksort#1^#(::(@z, @zs)) -> quicksort#2^#(split(@z, @zs), @z) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> append^#(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@xs) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> quicksort^#(@ys) } We apply the transformation 'usablerules' on the sub-problem: Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Wall-time: 0.510764s CPU-time: 4.908s Wall-time: 1.653055s CPU-time: 15.901s S) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak DPs: { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { append^#(@l, @ys) -> c_1(append#1^#(@l, @ys)) , append#1^#(::(@x, @xs), @ys) -> c_2(append^#(@xs, @ys)) , quicksort^#(@l) -> c_5(quicksort#1^#(@l)) , quicksort#1^#(::(@z, @zs)) -> c_6(quicksort#2^#(split(@z, @zs), @z), split^#(@z, @zs)) , quicksort#2^#(tuple#2(@xs, @ys), @z) -> c_7(append^#(quicksort(@xs), ::(@z, quicksort(@ys))), quicksort^#(@xs), quicksort^#(@ys)) , split^#(@pivot, @l) -> c_8(split#1^#(@l, @pivot)) , split#1^#(::(@x, @xs), @pivot) -> c_9(split^#(@pivot, @xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak Trs: { #abs(#0()) -> #0() , #abs(#neg(@x)) -> #pos(@x) , #abs(#pos(@x)) -> #pos(@x) , #abs(#s(@x)) -> #pos(#s(@x)) , #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , append(@l, @ys) -> append#1(@l, @ys) , append#1(::(@x, @xs), @ys) -> ::(@x, append(@xs, @ys)) , append#1(nil(), @ys) -> @ys , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksort(@l) -> quicksort#1(@l) , quicksort#1(::(@z, @zs)) -> quicksort#2(split(@z, @zs), @z) , quicksort#1(nil()) -> nil() , split(@pivot, @l) -> split#1(@l, @pivot) , quicksort#2(tuple#2(@xs, @ys), @z) -> append(quicksort(@xs), ::(@z, quicksort(@ys))) , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , split#1(::(@x, @xs), @pivot) -> split#2(split(@pivot, @xs), @pivot, @x) , split#1(nil(), @pivot) -> tuple#2(nil(), nil()) , split#2(tuple#2(@ls, @rs), @pivot, @x) -> split#3(#greater(@x, @pivot), @ls, @rs, @x) , split#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , split#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We decompose the input problem according to the dependency graph into the upper component { quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) } and lower component { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Further, following extension rules are added to the lower component. { quicksortD^#(@l) -> quicksortD#1^#(@l) , quicksortD#1^#(::(@z, @zs)) -> quicksortD#2^#(splitD(@z, @zs), @z) , quicksortD#1^#(::(@z, @zs)) -> splitD^#(@z, @zs) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@xs) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@ys) } TcT solves the upper component with certificate YES(O(1),O(n^1)). Sub-proof: ---------- We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { quicksortD^#(@l) -> c_10(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { quicksortD#1^#(::(@z, @zs)) -> c_11(quicksortD#2^#(splitD(@z, @zs), @z), splitD^#(@z, @zs)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_12(appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))), quicksortD^#(@xs), quicksortD^#(@ys)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { quicksortD^#(@l) -> c_1(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_2(quicksortD#2^#(splitD(@z, @zs), @z)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksortD^#(@xs), quicksortD^#(@ys)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We replace rewrite rules by usable rules: Weak Usable Rules: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { quicksortD^#(@l) -> c_1(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_2(quicksortD#2^#(splitD(@z, @zs), @z)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksortD^#(@xs), quicksortD^#(@ys)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: quicksortD#1^#(::(@z, @zs)) -> c_2(quicksortD#2^#(splitD(@z, @zs), @z)) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#0] = [0] [#neg](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#s](x1) = [1] x1 + [1] [#greater](x1, x2) = [0] [#compare](x1, x2) = [0] [#ckgt](x1) = [0] [::](x1, x2) = [1] x2 + [1] [nil] = [0] [appendD](x1, x2) = [0] [appendD#1](x1, x2) = [0] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [quicksortD](x1) = [0] [quicksortD#1](x1) = [0] [splitD](x1, x2) = [1] x2 + [0] [quicksortD#2](x1, x2) = [0] [#false] = [0] [#true] = [1] [splitD#1](x1, x2) = [1] x1 + [0] [splitD#2](x1, x2, x3) = [1] x1 + [1] [splitD#3](x1, x2, x3, x4) = [1] x2 + [1] x3 + [1] [#EQ] = [0] [#GT] = [0] [#LT] = [0] [#abs^#](x1) = [0] [#greater^#](x1, x2) = [0] [#ckgt^#](x1) = [0] [#compare^#](x1, x2) = [0] [append^#](x1, x2) = [0] [append#1^#](x1, x2) = [0] [appendD^#](x1, x2) = [0] [appendD#1^#](x1, x2) = [0] [quicksort^#](x1) = [0] [quicksort#1^#](x1) = [0] [quicksort#2^#](x1, x2) = [0] [split^#](x1, x2) = [0] [split#1^#](x1, x2) = [0] [quicksortD^#](x1) = [1] x1 + [0] [quicksortD#1^#](x1) = [1] x1 + [0] [quicksortD#2^#](x1, x2) = [1] x1 + [0] [splitD^#](x1, x2) = [0] [splitD#1^#](x1, x2) = [0] [split#2^#](x1, x2, x3) = [0] [split#3^#](x1, x2, x3, x4) = [0] [splitD#2^#](x1, x2, x3) = [0] [splitD#3^#](x1, x2, x3, x4) = [0] [c_10](x1) = [0] [c_11](x1, x2) = [0] [c_12](x1, x2, x3) = [0] [c] = [0] [c_1](x1) = [1] x1 + [0] [c_2](x1) = [1] x1 + [0] [c_3](x1, x2) = [1] x1 + [1] x2 + [0] This order satisfies following ordering constraints [splitD(@pivot, @l)] = [1] @l + [0] >= [1] @l + [0] = [splitD#1(@l, @pivot)] [splitD#1(::(@x, @xs), @pivot)] = [1] @xs + [1] >= [1] @xs + [1] = [splitD#2(splitD(@pivot, @xs), @pivot, @x)] [splitD#1(nil(), @pivot)] = [0] >= [0] = [tuple#2(nil(), nil())] [splitD#2(tuple#2(@ls, @rs), @pivot, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [splitD#3(#greater(@x, @pivot), @ls, @rs, @x)] [splitD#3(#false(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [tuple#2(::(@x, @ls), @rs)] [splitD#3(#true(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [tuple#2(@ls, ::(@x, @rs))] [quicksortD^#(@l)] = [1] @l + [0] >= [1] @l + [0] = [c_1(quicksortD#1^#(@l))] [quicksortD#1^#(::(@z, @zs))] = [1] @zs + [1] > [1] @zs + [0] = [c_2(quicksortD#2^#(splitD(@z, @zs), @z))] [quicksortD#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [0] >= [1] @xs + [1] @ys + [0] = [c_3(quicksortD^#(@xs), quicksortD^#(@ys))] Consider the set of all dependency pairs DPs: { 1: quicksortD^#(@l) -> c_1(quicksortD#1^#(@l)) , 2: quicksortD#1^#(::(@z, @zs)) -> c_2(quicksortD#2^#(splitD(@z, @zs), @z)) , 3: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksortD^#(@xs), quicksortD^#(@ys)) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {2}. These cover all (indirect) predecessors of dependency pairs {1,2,3}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { quicksortD^#(@l) -> c_1(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_2(quicksortD#2^#(splitD(@z, @zs), @z)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksortD^#(@xs), quicksortD^#(@ys)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { quicksortD^#(@l) -> c_1(quicksortD#1^#(@l)) , quicksortD#1^#(::(@z, @zs)) -> c_2(quicksortD#2^#(splitD(@z, @zs), @z)) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> c_3(quicksortD^#(@xs), quicksortD^#(@ys)) } We apply the transformation 'usablerules' on the sub-problem: Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded We return to the main proof. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak DPs: { quicksortD^#(@l) -> quicksortD#1^#(@l) , quicksortD#1^#(::(@z, @zs)) -> quicksortD#2^#(splitD(@z, @zs), @z) , quicksortD#1^#(::(@z, @zs)) -> splitD^#(@z, @zs) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@xs) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@ys) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 4: splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) , 6: quicksortD#1^#(::(@z, @zs)) -> quicksortD#2^#(splitD(@z, @zs), @z) , 7: quicksortD#1^#(::(@z, @zs)) -> splitD^#(@z, @zs) , 8: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))) } Trs: { quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_3) = {1}, Uargs(c_4) = {1}, Uargs(c_13) = {1}, Uargs(c_14) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#0] = [0] [#neg](x1) = [1] x1 + [0] [#pos](x1) = [1] x1 + [0] [#s](x1) = [1] x1 + [1] [#greater](x1, x2) = [0] [#compare](x1, x2) = [0] [#ckgt](x1) = [0] [::](x1, x2) = [1] x2 + [1] [nil] = [0] [appendD](x1, x2) = [1] x2 + [0] [appendD#1](x1, x2) = [1] x1 + [1] x2 + [0] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [quicksortD](x1) = [0] [quicksortD#1](x1) = [1] [splitD](x1, x2) = [1] x2 + [0] [quicksortD#2](x1, x2) = [0] [#false] = [0] [#true] = [0] [splitD#1](x1, x2) = [1] x1 + [0] [splitD#2](x1, x2, x3) = [1] x1 + [1] [splitD#3](x1, x2, x3, x4) = [1] x2 + [1] x3 + [1] [#EQ] = [0] [#GT] = [0] [#LT] = [0] [#abs^#](x1) = [0] [#greater^#](x1, x2) = [0] [#ckgt^#](x1) = [0] [#compare^#](x1, x2) = [0] [append^#](x1, x2) = [0] [append#1^#](x1, x2) = [0] [appendD^#](x1, x2) = [0] [appendD#1^#](x1, x2) = [0] [quicksort^#](x1) = [0] [quicksort#1^#](x1) = [0] [quicksort#2^#](x1, x2) = [0] [split^#](x1, x2) = [0] [split#1^#](x1, x2) = [0] [quicksortD^#](x1) = [1] x1 + [1] [quicksortD#1^#](x1) = [1] x1 + [1] [quicksortD#2^#](x1, x2) = [1] x1 + [1] [splitD^#](x1, x2) = [1] x2 + [0] [splitD#1^#](x1, x2) = [1] x1 + [0] [split#2^#](x1, x2, x3) = [0] [split#3^#](x1, x2, x3, x4) = [0] [splitD#2^#](x1, x2, x3) = [0] [splitD#3^#](x1, x2, x3, x4) = [0] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [1] x1 + [0] [c_13](x1) = [1] x1 + [0] [c_14](x1) = [1] x1 + [0] This order satisfies following ordering constraints [splitD(@pivot, @l)] = [1] @l + [0] >= [1] @l + [0] = [splitD#1(@l, @pivot)] [splitD#1(::(@x, @xs), @pivot)] = [1] @xs + [1] >= [1] @xs + [1] = [splitD#2(splitD(@pivot, @xs), @pivot, @x)] [splitD#1(nil(), @pivot)] = [0] >= [0] = [tuple#2(nil(), nil())] [splitD#2(tuple#2(@ls, @rs), @pivot, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [splitD#3(#greater(@x, @pivot), @ls, @rs, @x)] [splitD#3(#false(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [tuple#2(::(@x, @ls), @rs)] [splitD#3(#true(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [tuple#2(@ls, ::(@x, @rs))] [appendD^#(@l, @ys)] = [0] >= [0] = [c_3(appendD#1^#(@l, @ys))] [appendD#1^#(::(@x, @xs), @ys)] = [0] >= [0] = [c_4(appendD^#(@xs, @ys))] [quicksortD^#(@l)] = [1] @l + [1] >= [1] @l + [1] = [quicksortD#1^#(@l)] [quicksortD#1^#(::(@z, @zs))] = [1] @zs + [2] > [1] @zs + [1] = [quicksortD#2^#(splitD(@z, @zs), @z)] [quicksortD#1^#(::(@z, @zs))] = [1] @zs + [2] > [1] @zs + [0] = [splitD^#(@z, @zs)] [quicksortD#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] > [0] = [appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys)))] [quicksortD#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] >= [1] @xs + [1] = [quicksortD^#(@xs)] [quicksortD#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] >= [1] @ys + [1] = [quicksortD^#(@ys)] [splitD^#(@pivot, @l)] = [1] @l + [0] >= [1] @l + [0] = [c_13(splitD#1^#(@l, @pivot))] [splitD#1^#(::(@x, @xs), @pivot)] = [1] @xs + [1] > [1] @xs + [0] = [c_14(splitD^#(@pivot, @xs))] Consider the set of all dependency pairs DPs: { 1: appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , 2: appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , 3: splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , 4: splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) , 5: quicksortD^#(@l) -> quicksortD#1^#(@l) , 6: quicksortD#1^#(::(@z, @zs)) -> quicksortD#2^#(splitD(@z, @zs), @z) , 7: quicksortD#1^#(::(@z, @zs)) -> splitD^#(@z, @zs) , 8: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))) , 9: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@xs) , 10: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@ys) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {4,6,7,8}. These cover all (indirect) predecessors of dependency pairs {3,4,5,6,7,8,9,10}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Strict DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) } Weak DPs: { quicksortD^#(@l) -> quicksortD#1^#(@l) , quicksortD#1^#(::(@z, @zs)) -> quicksortD#2^#(splitD(@z, @zs), @z) , quicksortD#1^#(::(@z, @zs)) -> splitD^#(@z, @zs) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@xs) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@ys) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { quicksortD#1^#(::(@z, @zs)) -> splitD^#(@z, @zs) , splitD^#(@pivot, @l) -> c_13(splitD#1^#(@l, @pivot)) , splitD#1^#(::(@x, @xs), @pivot) -> c_14(splitD^#(@pivot, @xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^1)). Strict DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) } Weak DPs: { quicksortD^#(@l) -> quicksortD#1^#(@l) , quicksortD#1^#(::(@z, @zs)) -> quicksortD#2^#(splitD(@z, @zs), @z) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@xs) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@ys) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^1)) We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. DPs: { 2: appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , 4: quicksortD#1^#(::(@z, @zs)) -> quicksortD#2^#(splitD(@z, @zs), @z) } Trs: { #compare(#0(), #0()) -> #EQ() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #pos(@y)) -> #LT() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_3) = {1}, Uargs(c_4) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#0] = [1] [#neg](x1) = [1] x1 + [1] [#pos](x1) = [1] x1 + [1] [#s](x1) = [1] x1 + [1] [#greater](x1, x2) = [1] [#compare](x1, x2) = [1] [#ckgt](x1) = [1] [::](x1, x2) = [1] x2 + [1] [nil] = [0] [appendD](x1, x2) = [1] x1 + [1] x2 + [0] [appendD#1](x1, x2) = [1] x1 + [1] x2 + [0] [tuple#2](x1, x2) = [1] x1 + [1] x2 + [0] [quicksortD](x1) = [1] x1 + [0] [quicksortD#1](x1) = [1] x1 + [0] [splitD](x1, x2) = [1] x2 + [0] [quicksortD#2](x1, x2) = [1] x1 + [1] [#false] = [1] [#true] = [1] [splitD#1](x1, x2) = [1] x1 + [0] [splitD#2](x1, x2, x3) = [1] x1 + [1] [splitD#3](x1, x2, x3, x4) = [1] x1 + [1] x2 + [1] x3 + [0] [#EQ] = [0] [#GT] = [1] [#LT] = [0] [#abs^#](x1) = [0] [#greater^#](x1, x2) = [0] [#ckgt^#](x1) = [0] [#compare^#](x1, x2) = [0] [append^#](x1, x2) = [0] [append#1^#](x1, x2) = [0] [appendD^#](x1, x2) = [1] x1 + [0] [appendD#1^#](x1, x2) = [1] x1 + [0] [quicksort^#](x1) = [0] [quicksort#1^#](x1) = [0] [quicksort#2^#](x1, x2) = [0] [split^#](x1, x2) = [0] [split#1^#](x1, x2) = [0] [quicksortD^#](x1) = [1] x1 + [0] [quicksortD#1^#](x1) = [1] x1 + [0] [quicksortD#2^#](x1, x2) = [1] x1 + [0] [splitD^#](x1, x2) = [0] [splitD#1^#](x1, x2) = [0] [split#2^#](x1, x2, x3) = [0] [split#3^#](x1, x2, x3, x4) = [0] [splitD#2^#](x1, x2, x3) = [0] [splitD#3^#](x1, x2, x3, x4) = [0] [c_3](x1) = [1] x1 + [0] [c_4](x1) = [1] x1 + [0] [c_13](x1) = [0] [c_14](x1) = [0] This order satisfies following ordering constraints [#greater(@x, @y)] = [1] >= [1] = [#ckgt(#compare(@x, @y))] [#ckgt(#EQ())] = [1] >= [1] = [#false()] [#ckgt(#GT())] = [1] >= [1] = [#true()] [#ckgt(#LT())] = [1] >= [1] = [#false()] [appendD(@l, @ys)] = [1] @l + [1] @ys + [0] >= [1] @l + [1] @ys + [0] = [appendD#1(@l, @ys)] [appendD#1(::(@x, @xs), @ys)] = [1] @xs + [1] @ys + [1] >= [1] @xs + [1] @ys + [1] = [::(@x, appendD(@xs, @ys))] [appendD#1(nil(), @ys)] = [1] @ys + [0] >= [1] @ys + [0] = [@ys] [quicksortD(@l)] = [1] @l + [0] >= [1] @l + [0] = [quicksortD#1(@l)] [quicksortD#1(::(@z, @zs))] = [1] @zs + [1] >= [1] @zs + [1] = [quicksortD#2(splitD(@z, @zs), @z)] [quicksortD#1(nil())] = [0] >= [0] = [nil()] [splitD(@pivot, @l)] = [1] @l + [0] >= [1] @l + [0] = [splitD#1(@l, @pivot)] [quicksortD#2(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [1] >= [1] @xs + [1] @ys + [1] = [appendD(quicksortD(@xs), ::(@z, quicksortD(@ys)))] [splitD#1(::(@x, @xs), @pivot)] = [1] @xs + [1] >= [1] @xs + [1] = [splitD#2(splitD(@pivot, @xs), @pivot, @x)] [splitD#1(nil(), @pivot)] = [0] >= [0] = [tuple#2(nil(), nil())] [splitD#2(tuple#2(@ls, @rs), @pivot, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [splitD#3(#greater(@x, @pivot), @ls, @rs, @x)] [splitD#3(#false(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [tuple#2(::(@x, @ls), @rs)] [splitD#3(#true(), @ls, @rs, @x)] = [1] @ls + [1] @rs + [1] >= [1] @ls + [1] @rs + [1] = [tuple#2(@ls, ::(@x, @rs))] [appendD^#(@l, @ys)] = [1] @l + [0] >= [1] @l + [0] = [c_3(appendD#1^#(@l, @ys))] [appendD#1^#(::(@x, @xs), @ys)] = [1] @xs + [1] > [1] @xs + [0] = [c_4(appendD^#(@xs, @ys))] [quicksortD^#(@l)] = [1] @l + [0] >= [1] @l + [0] = [quicksortD#1^#(@l)] [quicksortD#1^#(::(@z, @zs))] = [1] @zs + [1] > [1] @zs + [0] = [quicksortD#2^#(splitD(@z, @zs), @z)] [quicksortD#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [0] >= [1] @xs + [0] = [appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys)))] [quicksortD#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [0] >= [1] @xs + [0] = [quicksortD^#(@xs)] [quicksortD#2^#(tuple#2(@xs, @ys), @z)] = [1] @xs + [1] @ys + [0] >= [1] @ys + [0] = [quicksortD^#(@ys)] Consider the set of all dependency pairs DPs: { 1: appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , 2: appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , 3: quicksortD^#(@l) -> quicksortD#1^#(@l) , 4: quicksortD#1^#(::(@z, @zs)) -> quicksortD#2^#(splitD(@z, @zs), @z) , 5: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))) , 6: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@xs) , 7: quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@ys) } Processor 'matrix interpretation of dimension 1' induces the complexity certificate YES(?,O(n^1)) on application of dependency pairs {2,4}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4,5,6,7}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> quicksortD#1^#(@l) , quicksortD#1^#(::(@z, @zs)) -> quicksortD#2^#(splitD(@z, @zs), @z) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@xs) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@ys) } Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { appendD^#(@l, @ys) -> c_3(appendD#1^#(@l, @ys)) , appendD#1^#(::(@x, @xs), @ys) -> c_4(appendD^#(@xs, @ys)) , quicksortD^#(@l) -> quicksortD#1^#(@l) , quicksortD#1^#(::(@z, @zs)) -> quicksortD#2^#(splitD(@z, @zs), @z) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> appendD^#(quicksortD(@xs), ::(@z, quicksortD(@ys))) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@xs) , quicksortD#2^#(tuple#2(@xs, @ys), @z) -> quicksortD^#(@ys) } We apply the transformation 'usablerules' on the sub-problem: Weak Trs: { #greater(@x, @y) -> #ckgt(#compare(@x, @y)) , #compare(#0(), #0()) -> #EQ() , #compare(#0(), #neg(@y)) -> #GT() , #compare(#0(), #pos(@y)) -> #LT() , #compare(#0(), #s(@y)) -> #LT() , #compare(#neg(@x), #0()) -> #LT() , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x) , #compare(#neg(@x), #pos(@y)) -> #LT() , #compare(#pos(@x), #0()) -> #GT() , #compare(#pos(@x), #neg(@y)) -> #GT() , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y) , #compare(#s(@x), #0()) -> #GT() , #compare(#s(@x), #s(@y)) -> #compare(@x, @y) , #ckgt(#EQ()) -> #false() , #ckgt(#GT()) -> #true() , #ckgt(#LT()) -> #false() , appendD(@l, @ys) -> appendD#1(@l, @ys) , appendD#1(::(@x, @xs), @ys) -> ::(@x, appendD(@xs, @ys)) , appendD#1(nil(), @ys) -> @ys , quicksortD(@l) -> quicksortD#1(@l) , quicksortD#1(::(@z, @zs)) -> quicksortD#2(splitD(@z, @zs), @z) , quicksortD#1(nil()) -> nil() , splitD(@pivot, @l) -> splitD#1(@l, @pivot) , quicksortD#2(tuple#2(@xs, @ys), @z) -> appendD(quicksortD(@xs), ::(@z, quicksortD(@ys))) , splitD#1(::(@x, @xs), @pivot) -> splitD#2(splitD(@pivot, @xs), @pivot, @x) , splitD#1(nil(), @pivot) -> tuple#2(nil(), nil()) , splitD#2(tuple#2(@ls, @rs), @pivot, @x) -> splitD#3(#greater(@x, @pivot), @ls, @rs, @x) , splitD#3(#false(), @ls, @rs, @x) -> tuple#2(::(@x, @ls), @rs) , splitD#3(#true(), @ls, @rs, @x) -> tuple#2(@ls, ::(@x, @rs)) } StartTerms: basic terms Strategy: innermost No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Wall-time: 0.508563s CPU-time: 4.893s Wall-time: 1.683276s CPU-time: 16.163s Hurray, we answered YES(O(1),O(n^2))